p:FinProbSpace, n:, X, Y:RandomVariable(p;n).
E(n;(x.(x * x) * x * x) o X + Y)
=
((E(n;(x.(x * x) * x * x) o X)
(+ ((4 * E(n;X * X * X * Y)) + (6 * E(n;X * X * Y * Y)))
(+ (4 * E(n;X * Y * Y * Y)))
(+ E(n;(x.(x * x) * x * x) o Y))
  

latex

Definitions	t  T, True, x:A. B(x), Outcome, {x:A| B(x)} , , x:AB(x), #$n, {i..j}, Type, f(a), r * s, , r + s, x.A(x), , P  Q, P  Q, T, s = t, P & Q, x:A  B(x), P  Q, <a, b>, False, A, A  B, X + Y, (x.F(x)) o X, q*X, X * Y, RandomVariable(p;n), FinProbSpace, E(n;F), x. t(x)
Lemmas	expectation-rv-scale, expectation-rv-add, rv-add wf, rv-scale wf, rv-mul wf, rv-compose wf, expectation wf, random-variable wf, nat wf, finite-prob-space wf, qmul over plus qrng, qmul comm qrng, qmul ac 1 qrng, qadd ac 1 q, qmul ident, qmul assoc qrng, mon assoc q, squash wf, true wf, q distrib, rationals wf, qadd wf, int inc rationals, qmul wf, int seg wf, p-outcome wf